p:FinProbSpace, n:, X:RandomVariable(p;n), q:. E(n;q*X) = (q * E(n;X))   

latex

Definitions	t  T, x:A. B(x), E(n;F), r * s, , x:AB(x), True, , P  Q, P  Q, P & Q, s = t, T, r + s, x:A  B(x), P  Q, <a, b>, False, A, A  B, {x:A| B(x)} , , ||as||, {i..j}, f(a), x.A(x), X + Y, q*X, RandomVariable(p;n), FinProbSpace, , #$n, rv-const(a)
Lemmas	expectation-linear, random-variable wf, nat wf, finite-prob-space wf, int seg wf, length wf1, qmul zero qrng, qadd wf, squash wf, true wf, qmul comm qrng, qadd comm q, mon ident q, rationals wf, rv-const wf, int inc rationals, qmul wf, expectation wf